$\forall$$T$:Type, $L$:$T$ List.
\\[0ex]$\neg$null($L$) $\Rightarrow$ ($\exists$$f$:($\mathbb{N}\rightarrow$$T$). $\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($\forall$$t$:$\mathbb{N}$. $\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& $f$(${\it t'}$) $=$ $x$))